Nuprl Lemma : no_repeats-merge
0,22
postcript
pdf
T
:Type.
T
(
bs
,
as
:
T
List. no_repeats(
T
;
as
)
sorted(
as
)
no_repeats(
T
;merge(
as
;
bs
)))
latex
Definitions
no_repeats(
T
;
l
)
,
x
:
A
.
B
(
x
)
,
sorted(
L
)
,
t
T
,
P
Q
,
merge(
as
;
bs
)
,
S
T
Lemmas
sorted-merge
,
sorted
wf
,
no
repeats
wf
,
s-insert-no-repeats
,
merge
wf
origin
T:Type.
(bs, as:T List. no_repeats(T;as) sorted(as) no_repeats(T;merge(as;bs))) T:Type.
(bs, as:T List. no_repeats(T;as) sorted(as) no_repeats(T;merge(as;bs))) x:A. B(x)
T Q T